$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $f$, $g$:$a$:$A$ fp$\rightarrow$ $B$($a$), ${\it eq}$:EqDecider($A$). $f$ $\oplus$ $g$ $\in$ $a$:$A$ fp$\rightarrow$ $B$($a$)